(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_NRA)
(declare-fun v0 () Real)
(declare-fun v1 () Real)
(declare-fun v2 () Real)
(assert (let ((e3 2))
(let ((e4 1))
(let ((e5 3))
(let ((e6 (- v0)))
(let ((e7 (* v2 (- e3))))
(let ((e8 (- v2 e7)))
(let ((e9 (* e5 v2)))
(let ((e10 (* e5 e6)))
(let ((e11 (+ v2 v0)))
(let ((e12 (* e11 e3)))
(let ((e13 (* e11 e7)))
(let ((e14 (- v1)))
(let ((e15 (- e13)))
(let ((e16 (- e12)))
(let ((e17 (/ e5 e5)))
(let ((e18 (+ e12 e6)))
(let ((e19 (- e9)))
(let ((e20 (+ v1 e15)))
(let ((e21 (+ e17 e6)))
(let ((e22 (/ e3 e5)))
(let ((e23 (- v2)))
(let ((e24 (/ e3 e4)))
(let ((e25 (distinct e23 e6)))
(let ((e26 (= e15 e9)))
(let ((e27 (= e11 e9)))
(let ((e28 (>= e22 e17)))
(let ((e29 (< e21 e19)))
(let ((e30 (< e13 e6)))
(let ((e31 (>= e12 e22)))
(let ((e32 (distinct e22 e12)))
(let ((e33 (< v0 e7)))
(let ((e34 (>= e11 e10)))
(let ((e35 (= e24 e20)))
(let ((e36 (< e7 e17)))
(let ((e37 (>= e15 e7)))
(let ((e38 (>= e7 e11)))
(let ((e39 (< v0 e17)))
(let ((e40 (< e17 e8)))
(let ((e41 (>= e17 v1)))
(let ((e42 (>= e20 e24)))
(let ((e43 (>= e9 e18)))
(let ((e44 (< e7 e22)))
(let ((e45 (= v1 e6)))
(let ((e46 (<= e22 e11)))
(let ((e47 (>= e19 e17)))
(let ((e48 (<= e19 e8)))
(let ((e49 (<= e12 e14)))
(let ((e50 (> e17 e17)))
(let ((e51 (> e13 e11)))
(let ((e52 (>= e19 v0)))
(let ((e53 (> v1 e16)))
(let ((e54 (= e16 e16)))
(let ((e55 (< e20 e17)))
(let ((e56 (> e19 e18)))
(let ((e57 (>= e18 e8)))
(let ((e58 (< v0 e7)))
(let ((e59 (< e8 e9)))
(let ((e60 (distinct e19 v1)))
(let ((e61 (= e17 e14)))
(let ((e62 (>= e16 e8)))
(let ((e63 (<= e16 e10)))
(let ((e64 (= e15 e7)))
(let ((e65 (> e22 e21)))
(let ((e66 (<= e16 e23)))
(let ((e67 (distinct e9 e22)))
(let ((e68 (<= e21 e19)))
(let ((e69 (distinct e23 e14)))
(let ((e70 (< e6 e23)))
(let ((e71 (> e11 e11)))
(let ((e72 (> e20 e6)))
(let ((e73 (= e14 e8)))
(let ((e74 (>= e13 v2)))
(let ((e75 (<= e7 e21)))
(let ((e76 (> e15 e18)))
(let ((e77 (<= e23 e10)))
(let ((e78 (< e10 e17)))
(let ((e79 (>= v0 v1)))
(let ((e80 (distinct v0 e9)))
(let ((e81 (= e14 e17)))
(let ((e82 (distinct e10 v2)))
(let ((e83 (<= e8 e15)))
(let ((e84 (= e14 e21)))
(let ((e85 (<= v2 e16)))
(let ((e86 (< e13 e12)))
(let ((e87 (> e19 e24)))
(let ((e88 (< e12 v2)))
(let ((e89 (< e15 e22)))
(let ((e90 (>= e21 e8)))
(let ((e91 (< e17 e22)))
(let ((e92 (= e8 e10)))
(let ((e93 (> e19 e7)))
(let ((e94 (= e19 e20)))
(let ((e95 (<= e18 e18)))
(let ((e96 (< e18 v0)))
(let ((e97 (< e22 v0)))
(let ((e98 (>= e18 v2)))
(let ((e99 (>= v0 v2)))
(let ((e100 (> e20 e23)))
(let ((e101 (= e18 e8)))
(let ((e102 (> e19 e9)))
(let ((e103 (< e19 e22)))
(let ((e104 (<= e20 e15)))
(let ((e105 (<= e11 e6)))
(let ((e106 (=> e84 e57)))
(let ((e107 (and e39 e47)))
(let ((e108 (ite e67 e75 e64)))
(let ((e109 (ite e94 e105 e28)))
(let ((e110 (or e65 e52)))
(let ((e111 (xor e36 e41)))
(let ((e112 (xor e48 e101)))
(let ((e113 (= e37 e70)))
(let ((e114 (= e38 e74)))
(let ((e115 (and e109 e26)))
(let ((e116 (xor e59 e91)))
(let ((e117 (or e45 e115)))
(let ((e118 (or e86 e63)))
(let ((e119 (ite e106 e78 e61)))
(let ((e120 (or e33 e76)))
(let ((e121 (xor e82 e79)))
(let ((e122 (= e27 e51)))
(let ((e123 (= e35 e114)))
(let ((e124 (ite e83 e44 e49)))
(let ((e125 (not e97)))
(let ((e126 (or e56 e120)))
(let ((e127 (xor e32 e103)))
(let ((e128 (= e126 e40)))
(let ((e129 (=> e72 e46)))
(let ((e130 (or e111 e80)))
(let ((e131 (not e50)))
(let ((e132 (ite e128 e113 e113)))
(let ((e133 (and e29 e81)))
(let ((e134 (ite e100 e131 e129)))
(let ((e135 (xor e43 e107)))
(let ((e136 (and e66 e102)))
(let ((e137 (= e99 e127)))
(let ((e138 (ite e118 e122 e77)))
(let ((e139 (xor e110 e89)))
(let ((e140 (or e54 e132)))
(let ((e141 (= e130 e92)))
(let ((e142 (xor e138 e34)))
(let ((e143 (not e73)))
(let ((e144 (ite e90 e140 e31)))
(let ((e145 (xor e144 e93)))
(let ((e146 (and e87 e96)))
(let ((e147 (=> e142 e55)))
(let ((e148 (or e98 e141)))
(let ((e149 (or e124 e125)))
(let ((e150 (ite e85 e117 e117)))
(let ((e151 (xor e60 e25)))
(let ((e152 (ite e134 e150 e133)))
(let ((e153 (and e136 e139)))
(let ((e154 (and e112 e108)))
(let ((e155 (and e69 e121)))
(let ((e156 (=> e95 e53)))
(let ((e157 (ite e119 e68 e145)))
(let ((e158 (ite e62 e152 e135)))
(let ((e159 (= e147 e71)))
(let ((e160 (= e157 e104)))
(let ((e161 (ite e149 e88 e160)))
(let ((e162 (and e159 e148)))
(let ((e163 (not e143)))
(let ((e164 (= e154 e137)))
(let ((e165 (= e146 e146)))
(let ((e166 (= e156 e155)))
(let ((e167 (or e42 e158)))
(let ((e168 (and e161 e163)))
(let ((e169 (=> e162 e165)))
(let ((e170 (and e167 e164)))
(let ((e171 (ite e30 e166 e153)))
(let ((e172 (or e171 e171)))
(let ((e173 (and e123 e58)))
(let ((e174 (xor e173 e116)))
(let ((e175 (not e170)))
(let ((e176 (and e169 e168)))
(let ((e177 (= e176 e172)))
(let ((e178 (not e177)))
(let ((e179 (=> e151 e178)))
(let ((e180 (ite e179 e175 e174)))
e180
)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
